perm filename BNF.PUB[BNF,JRA] blob sn#026683 filedate 1973-02-28 generic text, type T, neo UTF8
COMMENT ⊗   VALID 00004 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	.BEGIN DOUBLE SPACE
 00004 00003	.NEXT PAGE
 00006 00004	.NEXT PAGE
 00009 ENDMK
⊗;
.BEGIN DOUBLE SPACE

The parsers for the input syntax and the command language are both contstructed
by Lynn Quam's
Syntax Directed Input Output program.


.END

.NEXT PAGE
THE SIMPLE STRATEGY LANGUAGE
.BEGIN DOUBLE SPACE

The most straightforwrd application of the strategy language consists
of using Boolean combinations of the builtin strategies. 
.END
.BEGIN VERBATIM

<STRATEGY>::=<F1>;

<F1>	::=<F2>
	::=<F1><OR><F2>

<F2>	::=<F3>
        ::=<F2><AND><F3>

<F3>	::=(<F1>)
	::=<NOT><F3>
	::=<PREDIC>

<PREDIC>::=ANCESTRY
	::=NONE
	::=VINE
	::=UNIT
	::=P1
	::=SUPPORT[<C>]
	::=MODEL[<PREDLST>;<PREDLST>]
	::=EQUALITY[<OP>,<NUMBER>]
	::=DEMOD[<CLAUSES>,<NUMBER>]
	::=DEFMODEL[ID]
	::=LENGTH[<NUMBER>]
	::=DEPTH[<NUMBER>]

<PREDLST>
	::=<ID>,<PREDLST>
	::=<ID>
	::=


.END

.NEXT PAGE
THE INPUT FORMAT
.BEGIN DOUBLE SPACE
The usual form for input consists of the declarations of the non-logical
constituents of the axioms, followed by a sequence of statements.  The statements
may be assigned names, and if a statement named THEOREM is present that statement
is negated before being added to the memory of the prover.
.END
.BEGIN VERBATIM
<INPUT>	::=<DECOP>:<OPLIST>;
	::=<ID>:
	::=<S>

<DECOP>	::=VAR | INF_OP | INF_PRED | PRE_OP | PRE_PRED | EQUALITY

<OPLIST>::=<OP>,<OPLIST>
	::=<OP>

<S>	::=;
	::=<S1>;

<S1>	::=<S2>
	::=<S1><EQUIV><S2>

<S2>	::=<S3>
	::=<S2><IMP><S3>

<S3>	::=<S4>
	::=<S3><OR><S4>

<S4>	::=<S5>
	::=<S4><AND><S5>

<S5>	::=(<S1>)
	::=<NOT><S5>
	::=<QFF><BODY>
	::=<PRED>

<BODY>	::= <IVAR><S5>
	::=(<VARLIST>)<S5>

<VARLIST>::=<IVAR>,<VARLIST>
	::=<IVAR>
.END
.BEGIN DOUBLE SPACE

In the following,the routines corresponding to <PREPREDLET>, <INFPREDLET>, <IVAR>, <PREFN>, and
<INFN> check the lists of prefix- and infix- predicate and function letters, and
the variable list, all of which were manufactured by the appropriate declarations.

.END

.BEGIN VERBATIM

<PRED>  ::=<PREPREDLET><ITMLST>
	::=<TM><INFPREDLET><TM>

<ITMLST>::=(<ITMS>)

<ITMS>  ::=<TM><ITMS>
	::=<TM>

<TM>    ::=<IVAR>
	::=<PREFN><ITMLST>
	::=<PREFN>
	::=(<TM>)
	::=<TM><INFN><TM>


The logical connectives are defined as follows:

<EQUIV>	::= ≡ | ↔ 

<IMP>	::= ⊃

<OR>	::= ∨

<AND>	::= ∧

<NOT>	::= ¬

<QFF>	::= ∀ | ∃
.END